$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$), $P$:($A$$\rightarrow\mathbb{B}$), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ $X$$\mid$$a$.$P$($a$))) $\Rightarrow$ ($X$$\mid$$a$.$P$($a$)($e$) $\sim$ $X$($e$))